1. Technical Field
The present invention relates to evaluating the performance of data processing systems. More specifically, the present invention relates to quantifying average performance characteristics.
2. Description of Related Art
Performance metrics attempt to quantify some aspect of system performance, examples include load latencies, cycles-per-instruction measurements, cache hit ratios, and arbitration delay and/or fairness. In extreme cases, performance problems may even yield livelock/deadlock conditions, in which the system gets xe2x80x9cstuckxe2x80x9d and can make no forward progress in an execution.
Most performance evaluations are calculated with respect to a set of specific test, sometimes referred to as a benchmark. Such evaluations consider aspects such as minimum values, maximum values, and average values of the performance metric. While such evaluation procedures are easy to visualize, and are quite useful with a meaningful set of tests, they suffer from not providing insight into true system performance with respect to any arbitrary test. Consequently, tests may fail to consider sequences of execution which expose worst-case behavior of the design under test. This fundamental limitation has been noted by many in the industry.
Formal verification is a rigorous validation approach; it uses mathematical reasoning to exhaustively verify the correctness of the design under test. It may reason about possibly infinite streams of execution, and in being exhaustive it may fully characterize the design under all possible streams of execution. The non-determinism supported by formal verification tools renders formal methods an attractive option for performance characterization.
Formal methods may be used to characterize absolute worst-case and best-case system performance. However, there is no manner in which a model checking framework will allow measurement of average performance along all paths. While model checking is a branching-time framework, allowing quantification at any point in time over xe2x80x9cany pathxe2x80x9d or xe2x80x9call pathsxe2x80x9d, it does not allow counting of these paths. Furthermore, model checkers typically do not consider the probability of a path. Typically they count a transition with probability 1/100,000 than same as a transition with probability 99999/100,000. Thus, model checkers are quite different than simulators (where the transition with probability 1/100,000 is not likely to ever be considered).
Therefore, an enhancement to existing formal verification tools that would allow direct characterization of average performance would be desirable.
The present invention provides a method for characterizing average performance in a data processing system. This method consists of adding meta-tool level variables to a verification tool. These meta-tool variables keep track, at once, of all concurrent streams of execution that the tool is considering in its reachability analysis. The image of an initial state variable is found and then divided into a frontier of new states and a set of previously reached states. The previously reached states are ignored and the image of the frontier is found. This process continues until the frontier is empty and all possible states have been reached. In one embodiment of the present invention, the probabilities of the paths can be considered by sampling and holding input data using SMV (a model checking tool) variables.